ra, rt:(IdId). Inj(Id; Id; rt)  Inj(Id; Id; ra)  Inj(Knd; Knd; k.kind-rename(ra;rt;k)) 

latex

Definitions	t  T, P  Q, x:A. B(x), Id, s = t, True, T, locl(a), IdLnk, rcv(l,tg), Knd, P & Q, f(a), {T}, False, x:AB(x), left+right, tag(k), lnk(k), act(k), islocal(k), kindcase(k; a.f(a); l,t.g(l;t) ), x:AB(x), Prop, x,y. t(x;y), x. t(x), Inj(A; B; f), kind-rename(ra;rt;k)
Lemmas	kindcase wf, Knd wf, not locl rcv, not rcv locl, locl one one, rcv one one, rcv wf, IdLnk wf, locl wf, squash wf, true wf, Id wf